↑ More generally, in a formal system, rules restrict the use of primitive notions. See e.g. MU puzzle for a non-logical formal system.
↑ Euclid (300 B.C.) still gave definitions in his Elements, like "A line is breadthless length".
↑ This axiom can be formalized in predicate logic as "∀x1,x2∈P. ∃y∈L. C(y,x1) ∧ C(y,x2)", where P, L, and C denotes the set of points, of lines, and the "contains" relation, respectively.
